{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators, GADTs,
  FlexibleInstances, MultiParamTypeClasses, FlexibleContexts, UndecidableInstances,
  TypeSynonymInstances, EmptyDataDecls #-}

{-# OPTIONS_GHC -fcontext-stack=250 #-}

{- |

Module      :  Examples.LLGeneric
Copyright   :  (c) The University of Kansas 2011
License     :  BSD3

Maintainer  :  nicolas.frisby@gmail.com
Stability   :  experimental
Portability :  see LANGUAGE pragmas (... GHC)

The declaration that hook 'Examples.LLBase.Term' into @yoko@. This will
eventually be generated via Template Haskell.

-}
module Examples.LLGeneric where

import Examples.LLBase (Term)
import qualified Examples.LLBase as B

import Examples.ReflectAux

data DVar; data Var; data App

concat `fmap` mapM derive [''Term, ''DVar, ''Var, ''App]

type instance Tag DVar = $(return $ encode "DVar")
type instance Range DVar = Term
instance DC DVar where
  occName _ = "DVar"
  fr ~(DVar i) = B.DVar i
data instance RM m (N DVar) = DVar Int
type instance Tag Var = $(return $ encode "Var")
type instance Range Var = Term
instance DC Var where
  occName _ = "Var"
  fr ~(Var i) = B.Var i
data instance RM m (N Var) = Var Int
type instance Tag App = $(return $ encode "App")
type instance Range App = Term
instance DC App where
  occName _ = "App"
  fr ~(App tm0 tm1) = B.App tm0 tm1
data instance RM m (N App) = App (Med m Term) (Med m Term)
data instance DCs Term dc where
  DVar_ :: DCs Term DVar; Var_ :: DCs Term Var
  App_ :: DCs Term App
type instance DTs Term = TermDTs
instance DT Term where
  packageName _ = "datatype-reflect"
  moduleName _ = "TermBase"
  disband (B.DVar i)      = disbanded $ DVar i
  disband (B.Var i)       = disbanded $ Var i
  disband (B.App tm0 tm1) = disbanded $ App tm0 tm1
type instance Fin (DCs Term) = ((:=:) DVar :|| (:=:) Var) :|| (:=:) App
instance Finite (DCs Term) where
  toFin DVar_ = membership; toFin Var_ = membership; toFin App_ = membership
  predFin _ _ x = x
instance Etinif (DCs Term) where
  frFin x = case x of
    LeftU (LeftU  Refl) -> DVar_
    LeftU (RightU Refl) -> Var_
    RightU Refl  -> App_

data TermDTs t where Term__ :: TermDTs Term
type instance Fin TermDTs = (:=:) Term
instance Finite TermDTs where toFin Term__ = membership; predFin _ _ x = x
instance Etinif TermDTs where frFin Refl = Term__

finite_set [t|TermDTs|]



type instance Rep DVar = D Int :* U
instance Generic DVar where
  rep ~(DVar i) = D i :* U
  obj ~(D i :* U) = DVar i
type instance Rep Var = D Int :* U
instance Generic Var where
  rep ~(Var i) = D i :* U
  obj ~(D i :* U) = Var i
type instance Rep App = R Term :* R Term :* U
instance Generic App where
  rep ~(App tm0 tm1) = R tm0 :* R tm1 :* U
  obj ~(R tm0 :* R tm1 :* U) = App tm0 tm1
